effective(e) == e':E(Sys). e'':E(Out). (e is f*(e') & e' loc e'' ) 

latex

---

clarification:

cr-effective(es;Sys;Out;f;e)
== e':es-E-interface(es;Sys)
== e'':es-E-interface(es;Out)
== (fun-connected(es-E-interface(es;Sys);f;e';e) & es-le(es;e';e'')) 

latex

Up	abstract chain replication
Wellformedness Lemmas	cr-effective wf
Definitions	x:A. B(x), P & Q, y is f*(x), E(X), e loc e'
FDL editor aliases	cr-effective